$\forall$$T$:Type, $x$:$T$, $a$:Atom1. AtomFree(Type;$T$) $\Rightarrow$ $x$:$T$$>>$$a$ $\in$ Prop